Nuprl Lemma : neg_assert_of_eq_atom
13,42
postcript
pdf
x
,
y
:Atom. (
(
x
=a
y
))
x
y
Atom
latex
Up
bool
1
,
bool
1
Definitions
a
b
T
,
,
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
x
:
A
.
B
(
x
)
Lemmas
nequal
wf
,
eq
atom
wf
,
assert
wf
,
not
wf
origin